Inference at * 1 1 1 1 
Iof proof for Lemma dep ax choice:



1. A : Type
2. B : AType
3. Q : x:AB(x)Type
4. g : x:Ay:B(x)  Q(x,y)
5. x : A
6. y : y:B(x)  Q(x,y)
7. y = g(x)
  Q(x,(g(x)).1) 

latex

 by D 6 

latex

 1: 

 1: 6. y1 : B(x)
 1: 7. y2 : Q(x,y1)
 1: 8. <y1, y2> = g(x)
 1:   Q(x,(g(x)).1)
 .

Definitions

x:A  B(x)